/*
 *  SableJBDD, a Java Binary Decision Diagram package.
 *  Copyright (C) 2004  Feng Qian
 *
 *  This library is free software; you can redistribute it and/or
 *  modify it under the terms of the GNU Lesser General Public
 *  License as published by the Free Software Foundation; either
 *  version 2.1 of the License, or (at your option) any later version.
 *
 *  This library is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 *  Lesser General Public License for more details.
 *
 *  You should have received a copy of the GNU Lesser General Public
 *  License along with this library; if not, write to the Free Software
 *  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */
//$Id: ReclaimableNodePool.java,v 1.6 2004/03/15 02:07:09 fqian Exp $
package SableJBDD.bdd.internal;

import SableJBDD.bdd.*;
import java.io.PrintStream;
import java.lang.ref.*;
import java.lang.reflect.*;

/**
 * A reclaimable node pool creates a phantom reference for each newly created node.
 * Any unreachable node is put in a reference queue, and it recycles reference
 * queue at certain time. 
 *
 * @author Feng Qian
 */
public abstract class ReclaimableNodePool extends BddNodePool{
  // each node is hold by a phantom reference
  protected ReferenceQueue refq;
  protected PhantomNode    refs, lastref;

  // phantom node queue size
  protected int phantomQueueSize;

  // profiling info
  private int numberOfRecycleEvents = 0;
  private int numberOfRecycledNodes = 0;

  protected static Field referent_field;
  static {
    try {
      referent_field = Reference.class.getDeclaredField("referent");
    } catch (Exception e) {
      e.printStackTrace();
      System.exit(1);
    }
  }

  class PhantomNode extends PhantomReference {
    PhantomNode next;
    PhantomNode(JBddNode node, ReferenceQueue q, PhantomNode next) {
      super(node, q);
      this.next = next;
    }
  }
  
  /**
   * Defines a pool with an initial number of pre-allocated nodes.
   * Creates a phontom reference for each node.
   */
  public ReclaimableNodePool (int size) {
    super(size);
    this.refq = new ReferenceQueue();
    JBddNode node = super.head;
    this.lastref = new PhantomNode(node, this.refq, null);
    this.refs    = this.lastref;

    int i = 1;
    node = node.getNext();
    while (node != null) {
      i++;
      this.refs = new PhantomNode(node, this.refq, this.refs);
      node = node.getNext();
    }
    this.phantomQueueSize = size;
    // assert size == i;
  }

  /**
   * Gets a node from a pool either by reusing an existing node
   * or by creating a new object.
   * NOTE: a JBddNode is a unique object, 
   */
  public JBddNode getFreshNode(JBddVariable var, 
                               JBddNode low, 
                               JBddNode high) {
    // good time to check the queue.
    if (super.empty()) {System.gc(); recycle();}
    return super.getFreshNode(var, low, high);
  }

  // going throw phantom reference queue and pick up dead nodes.
  private synchronized void recycle() {
    this.numberOfRecycleEvents ++;
    for (;;) {
      Reference ref = this.refq.poll();
      if (ref == null) return;
      try {
        referent_field.setAccessible(true);
        JBddNode node = (JBddNode)referent_field.get(ref);
        referent_field.setAccessible(false);
        // assert node != null;
        node.reclaim();
        add(node);
        this.numberOfRecycledNodes ++;
      } catch (Exception e) {
        System.err.println("unable to recycle objects");
        e.printStackTrace();
      }
    }
  }
  
  public void reportStatistics(PrintStream out) {
    out.println("ReclaimableNodePool : ");
    super.reportStatistics(out);
    out.println("       recycle events : "+this.numberOfRecycleEvents);
    out.println("       recycled nodes : "+this.numberOfRecycledNodes); 
  }
}
